#include "solver.h"

/* X <> Y, T = True ; X = Y, T = false */
void setup_turnover(int X, int Y, int T, solver *s)
{
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	veci_resize (&lits,0);
	var = X;
	veci_push (&lits, lit_neg (toLit (var)));
	var = Y;
	veci_push (&lits, toLit (var));
	var = T;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = X;
	veci_push (&lits, toLit (var));
	var = Y;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = X;
	veci_push (&lits, toLit (var));
	var = Y;
	veci_push (&lits, toLit (var));
	var = T;
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = X;
	veci_push (&lits, lit_neg (toLit (var)));
	var = Y;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);
}

/* C00 : C[m][n] ; C10 : C[m-1][n] ; C11 : C[m-1][n-1] ; T : T[m] */
void step_formula0 (int C00, int C10, int C11, int T, solver *s)
{
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	veci_resize (&lits,0);
	var = C00;
	veci_push (&lits, toLit (var));
	var = C10;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C00;
	veci_push (&lits, toLit (var));
	var = C11;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C00;
	veci_push (&lits, lit_neg (toLit (var)));
	var = C10;
	veci_push (&lits, toLit (var));
	var = C11;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C00;
	veci_push (&lits, lit_neg (toLit (var)));
	var = C10;
	veci_push (&lits, toLit (var));
	var = T;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C00;
	veci_push (&lits, lit_neg (toLit (var)));
	var = C11;
	veci_push (&lits, toLit (var));
	var = T;
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);
}

/* C0 : C[m][0] ; C1 : C[m-1][0] ; T : T[m] */
void step_formula1 (int C0, int C1, int T, solver *s)
{
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	veci_resize (&lits,0);
	var = C0;
	veci_push (&lits, toLit (var));
	var = C1;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C0;
	veci_push (&lits, lit_neg (toLit (var)));
	var = C1;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C0;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);
}

/* C0 : C[m][m] ; C1 : C[m-1][m-1] ; T : T[m] */
void step_formula2 (int C0, int C1, int T, solver *s)
{
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	veci_resize (&lits,0);
	var = C0;
	veci_push (&lits, toLit (var));
	var = C1;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C0;
	veci_push (&lits, lit_neg (toLit (var)));
	var = C1;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = C0;
	veci_push (&lits, lit_neg (toLit (var)));
	var = T;
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);
}

/* requiring among T[L] only num variables are true */
/* C[i][j] is true: among T[0],...T[i-1] only j variables are true */
int counter_positive1 (int L, int T[L], int num, int num2, int C[L + 1][num2 + 1], solver *s, int base)
{
	int i, j, m, n;

	/* setup the no. of logical variable C */
	for (i = 0; i < L; i++)
	{
		for (j = 0; j < num + 1; j++)
		{
			C[i + 1][j] = base + i * (num + 1) + j;
		}
	}

	/* setup the initial value */
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	if (num)
		C[1][1] = T[0];

	veci_resize (&lits,0);
	var = C[1][0];
	veci_push (&lits, toLit (var));
	var = T[0];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));
        
	veci_resize (&lits,0);
	var = C[1][0];
	veci_push (&lits, lit_neg (toLit (var)));
	var = T[0];
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));
        
	for (i = 2; i <= L - num; i++)
	{
		step_formula1 (C[i][0], C[i - 1][0], T[i - 1], s);
	}

	veci_resize (&lits,0);
	var = C[L][num];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);
	
	/* setup the step formula */
	for (i = 0; i < num; i++)
	{
		m = L - i;
		if (m < 2)
			break;
		for (j = 0; j <= i; j++)
		{
			n = num - j;
			if (n > 0)
			{
				if (m > n)
				{
					step_formula0 (C[m][n], C[m - 1][n], C[m - 1][n - 1], T[m - 1], s);
				}
				else if (m == n && m > 1)
				{
					step_formula2 (C[m][n], C[m - 1][n - 1], T[m - 1], s);
				}
			}
		}
	}

	for (i = L - num; i > num; i--)
	{
		m = i;
		for (j = 0; j <= num; j++)
		{
			n = j;
			if (n > 0)
			{
				if (m > n)
				{
					step_formula0 (C[m][n], C[m - 1][n], C[m - 1][n - 1], T[m - 1], s);
				}
				else if (m == n && m > 1)
				{
					step_formula2 (C[m][n], C[m - 1][n - 1], T[m - 1], s);
				}
			}
		}
	}

	for (i = (num < L - num) ? num : L - num; i >= 2; i--)
	{
		m = i;
		for (j = 0; j <= i; j++)
		{
			n = j;
			if (n > 0)
			{
				if (m > n)
				{
					step_formula0 (C[m][n], C[m - 1][n], C[m - 1][n - 1], T[m - 1], s);
				}
				else if (m == n && m > 1)
				{
					step_formula2 (C[m][n], C[m - 1][n - 1], T[m - 1], s);
				}
			}
		}
	}

	return base + L * (num + 1);
}

/* requiring that the appearance of 1 in X array is earlier than Y array */
int check_order1 (int N, int X[N], int Y[N], solver *s, int base)
{
	int i;
	int F[N];

	for (i = 0; i < N; i++)
	{
		F[i] = base + i;
	}
	
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	/* setup the variable F[N - 1] */
	veci_resize (&lits,0);
	var = F[N - 1];
	veci_push (&lits, toLit (var));
	var = X[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	var = Y[N - 1];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = F[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	var = X[N - 1];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = F[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	var = Y[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	/* setup the variable F[i] */
	for (i = 0; i < N - 1; i++)
	{
		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, toLit (var));
		var = X[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = Y[i];
		veci_push (&lits, toLit (var));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, toLit (var));
		var = Y[i];
		veci_push (&lits, toLit (var));
		var = F[i + 1];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = X[i];
		veci_push (&lits, toLit (var));
		var = F[i + 1];
		veci_push (&lits, toLit (var));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = Y[i];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));
	}

	/* require F[0] = 1 */
	veci_resize (&lits,0);
	var = F[0];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);

	return base + N;
}

/* requiring that the appearance of 1 in X array is not later than Y array */
int check_order2 (int N, int Y[N], int X[N], solver *s, int base)
{
	int i;
	int F[N];

	for (i = 0; i < N; i++)
	{
		F[i] = base + i;
	}
	
	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	/* setup the variable F[N - 1] */
	veci_resize (&lits,0);
	var = F[N - 1];
	veci_push (&lits, toLit (var));
	var = X[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	var = Y[N - 1];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = F[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	var = X[N - 1];
	veci_push (&lits, toLit (var));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_resize (&lits,0);
	var = F[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	var = Y[N - 1];
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	/* setup the variable F[i] */
	for (i = 0; i < N - 1; i++)
	{
		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, toLit (var));
		var = X[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = Y[i];
		veci_push (&lits, toLit (var));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, toLit (var));
		var = Y[i];
		veci_push (&lits, toLit (var));
		var = F[i + 1];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = X[i];
		veci_push (&lits, toLit (var));
		var = F[i + 1];
		veci_push (&lits, toLit (var));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = F[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = Y[i];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));
	}

	/* require F[0] = 0 */
	veci_resize (&lits,0);
	var = F[0];
	veci_push (&lits, lit_neg (toLit (var)));
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	veci_delete (&lits);

	return base + N;
}

/* prevention the early fix point */
int prevent_early_fixpoint (int N, int L, int S[L][N], solver *s, int base)
{
	int i;

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	int X[N];

	veci_resize (&lits,0);
	for (i = 0; i < N; i++)
	{
		X[i] = base + i;
		var = X[i];
		veci_push (&lits, toLit (var));
	}
	begin = veci_begin (&lits);
	solver_addclause (s, begin, begin + veci_size (&lits));

	for (i = 0; i < N; i++)
	{
		veci_resize (&lits,0);
		var = X[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = S[L - 3][i];
		veci_push (&lits, toLit (var));
		var = S[L - 2][i];
		veci_push (&lits, toLit (var));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = X[i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = S[L - 3][i];
		veci_push (&lits, lit_neg (toLit (var)));
		var = S[L - 2][i];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));
	}

	veci_delete (&lits);

	return base + N;
}

/* set fix point */
void set_fixpoint (int N, int L, int S[L][N], solver *s)
{
	int i;

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < N; i++)
	{
		veci_resize (&lits,0);
		var = S[L - 1][i];
		veci_push (&lits, toLit (var));
		var = S[L - 2][i];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		var = S[L - 2][i];
		veci_push (&lits, toLit (var));
		var = S[L - 1][i];
		veci_push (&lits, lit_neg (toLit (var)));
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));
	}

	veci_delete (&lits);
}

/* setup the known values in the pathway */
void set_pathway (int N, int L, int pathway[L][N], int S[L][N], solver *s)
{
	int i, j;

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			veci_resize (&lits,0);
			var = S[i][j];
			if (pathway[i][j] == 1)
			{
				veci_push (&lits, toLit (var));
			}
			else if (pathway[i][j] == 0)
			{
				veci_push (&lits, lit_neg (toLit (var)));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));
		}
	}

	veci_delete (&lits);
}

/* no all '0'/'1' node in the patheay */
void forbidden_noflip (int N, int L, int S[L][N], solver *s)
{
	int i, j;

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < N; i++)
	{
		veci_resize (&lits,0);
		for (j = 0; j < L - 1; j++)
		{
			var = S[j][i];
			veci_push (&lits, toLit (var));
		}
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));

		veci_resize (&lits,0);
		for (j = 0; j < L - 1; j++)
		{
			var = S[j][i];
			veci_push (&lits, lit_neg (toLit (var)));
		}
		begin = veci_begin (&lits);
		solver_addclause (s, begin, begin + veci_size (&lits));
	}

	veci_delete (&lits);
}
